Inference at * 2 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. (||l1||  ||l2||) c (i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)]))
  fseg(T;l1;l2) 

latex

 by ((D (-1)) 
CollapseTHEN (Unfold `fseg` ( 0))) 

latex

C1: 

C1: 4. ||l1||  ||l2||
C1: 5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
C1:   L:T List. (l2 = (L @ l1))
C.

Definitions

A c B, x:A  B(x), fseg(T;L1;L2)